package systemf





trait SystemFEvaluator extends Evaluator{ self: Evaluator with SubstitutionProvider =>

override def evaluate(t: LTerm) : LTerm= {
  try {
  val t_bis = eval1 (t)
  evaluate (t_bis)
  } 
  catch { case e: NoReductionPossibleExc => t }
}
  def eval1(t: LTerm): LTerm = t match {
    //E-IfTrue, E-IfFalse
    case If(c,p,n) if (isValue(c))            
      => if (c equals Tru) p else n
    //E-If
    case If(c,p,n)
      => If(eval1(c),p,n)
    
    //E-AppAbs
    case App( Lam(s,ty,t12), v2) if (isValue(v2))
      => substituteterm(v2).asTop.intoterm(t12)    
      //termSubstTop(v2,t12)
    //E-App2 
    case App(v1, t2)           if (isValue(v1))  
      => App(v1 ,eval1(t2))
    //E-App1
    case App(t1, t2)                             
      => App(eval1(t1), t2)
    
      
     
    //E-TAppAbs
    case TApp( TLam(s,t12), ty)                    
      => substitutetype(ty).asTop.intoterm(t12)    
      //typeintotermSubstTop(ty, t12)
    //E-TApp
    case TApp(t1, ty)
      => TApp(eval1(t1), ty)
      
    //E-UnpackPack
    case Unpack(Pack(impltype,implvar,pubtype),bodytyname,bodyvarname,body) if (isValue(implvar))
      => substitutetype(impltype).asTop.intoterm(
             substituteterm(implvar).asTop.intoterm(body)) 
      //       typeintotermSubstTop(impltype, termSubstTop(implvar, body))
    //E-Unpack
    case Unpack(impl,bodytyname,bodyvarname,body)
      => Unpack(eval1(impl),bodytyname,bodyvarname,body)
      
    //E-Pack
    case Pack(ty11,t12,pubtype)
      => Pack(ty11,eval1(t12),pubtype)
      
    //E-Let
    case Let(VarName(n),v1,tbody) if (isValue(v1))  
      => substituteterm(v1).asTop.intoterm(tbody)
         //  termSubst(0,v1,tbody)
    case Let(VarName(n),t1,t2)                      
      => Let(VarName(n),eval1(t1),t2)
    
    //E-RecProj
    case RecProj(r@Record(fields),label) 
      if ( isValue(r))   =>
           fields.filter( { case (n,f) => (n == label)}).map(_ _2).head
    case RecProj(Record(fields), label) =>
      def eval1first(fs:List[(String,LTerm)]) :List[(String,LTerm)]= {
        val h = fs.head
        if (isValue(h._2)) h::eval1first(fs.tail)
        else (h._1,eval1(h._2))::fs.tail
      }
      RecProj(Record(eval1first(fields)), label)
    case RecProj(t, label)                =>
      RecProj(eval1(t), label)
      
    case _                                    =>
         throw NoReductionPossibleExc
  }
  
  
  
  def isValue(t: LTerm) : Boolean= t match {
    case Lam(_,_,_) => true
    case TLam(_,_ ) => true
    case Lit(v)   => true
    case Tru()    => true
    case Fls()    => true
    case Unit()   => true
    case Pack(ty1,v,pubtype) => isValue(v)
    
    case Record(fields) => fields.map(_ _2) forall(isValue)
    case _        => false
  }
  
  
}




